Challenge 25: Verify safety of VecDeque by Samuelsills · Pull Request #564 · model-checking/verify-rust-std

Samuelsills · 2026-03-24T16:33:58Z

Summary

Verify all 43 functions listed in Challenge 25. 44 Kani proof harnesses, 0 failures.

Part A (13 unsafe functions): Safety contracts and proof_for_contract harnesses for buffer_read, buffer_write, buffer_range, push_unchecked, copy, copy_nonoverlapping, copy_slice, wrap_copy, write_iter, write_iter_wrapping, handle_capacity_increase, from_contiguous_raw_parts_in, abort_shrink.

Part B (30 safe abstractions): Proof harnesses for get, get_mut, swap, reserve, try_reserve, shrink_to, truncate, as_slices, as_mut_slices, range, range_mut, drain, pop_front, pop_back, push_front, push_back, insert, remove, split_off, append, retain_mut, grow, resize_with, make_contiguous, rotate_left, rotate_right, and others.

All harnesses exercise returned values to ensure full unsafe path coverage.

Resolves #286

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Verify all 43 functions listed in the challenge specification. 44 Kani proof harnesses, 0 failures. Resolves model-checking#286 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Samuelsills · 2026-03-29T15:59:32Z

Verification Coverage Report

Unsafe Functions (13/13 — contracts written and verified)

#	Function	Verified
1	`push_unchecked`	✅
2	`buffer_read`	✅
3	`buffer_write`	✅
4	`buffer_range`	✅
5	`copy`	✅
6	`copy_nonoverlapping`	✅
7	`wrap_copy`	✅
8	`copy_slice`	✅
9	`write_iter`	✅
10	`write_iter_wrapping`	✅
11	`handle_capacity_increase`	✅
12	`from_contiguous_raw_parts_in`	✅
13	`abort_shrink`	✅

Safe Abstractions (30/30 — absence of UB verified)

#	Function	Verified
1-30	`get`, `get_mut`, `swap`, `reserve_exact`, `reserve`, `try_reserve_exact`, `try_reserve`, `shrink_to`, `truncate`, `as_slices`, `as_mut_slices`, `range`, `range_mut`, `drain`, `pop_front`, `pop_back`, `push_front`, `push_back`, `insert`, `remove`, `split_off`, `append`, `retain_mut`, `grow`, `resize_with`, `make_contiguous`, `rotate_left`, `rotate_right`, `rotate_left_inner`, `rotate_right_inner`	✅ All 30

UBs Checked (automatic via Kani/CBMC)

✅ Accessing dangling or misaligned pointers
✅ Reading from uninitialized memory
✅ Mutating immutable bytes
✅ Producing an invalid value

Verification Approach

Tool: Kani Rust Verifier
44 proof harnesses total
Generic type T instantiated as concrete types for tractability
CBMC exhaustively checks all pointer operations for the listed UBs

Copilot

Pull request overview

This PR adds Kani-focused safety contracts (#[requires]) and proof harnesses to validate the safety of a large set of VecDeque operations, and updates the Challenge 25 documentation with a verification summary.

Changes:

Added #[requires] contracts (and some #[kani::modifies] annotations) to several internal VecDeque unsafe fns.
Added a substantial #[cfg(kani)] verification module with #[kani::proof] and #[kani::proof_for_contract] harnesses for VecDeque.
Updated the Challenge 25 markdown with a “Verification Summary” and mapping of functions to harnesses/contracts.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 6 comments.

File	Description
`library/alloc/src/collections/vec_deque/mod.rs`	Adds safety contracts to `VecDeque` internals and introduces many Kani proof harnesses in `mod verify`.
`doc/src/challenges/0025-vecdeque.md`	Adds a verification summary section and tables describing covered functions/contracts/harnesses.

Comments suppressed due to low confidence (1)

library/alloc/src/collections/vec_deque/mod.rs:517

write_iter writes to dst + i for every element yielded by iter without any bounds check, but its #[requires] only enforces dst < capacity(). The contract should capture the stated safety requirement that the iterator yields no more than capacity() - dst items (e.g., via an upper-bound from size_hint() or by requiring an ExactSizeIterator/TrustedLen), otherwise the contract is unsound and the body can write past the buffer.

    /// Writes all values from `iter` to `dst`.
    ///
    /// # Safety
    ///
    /// Assumes no wrapping around happens.
    /// Assumes capacity is sufficient: `dst + iter.len() <= capacity`.
    #[inline]
    #[requires(dst < self.capacity())]
    #[cfg_attr(kani, kani::modifies(
        core::ptr::slice_from_raw_parts_mut(self.ptr(), self.capacity()),
        written
    ))]
    unsafe fn write_iter(
        &mut self,
        dst: usize,
        iter: impl Iterator<Item = T>,
        written: &mut usize,
    ) {
        iter.enumerate().for_each(|(i, element)| unsafe {
            self.buffer_write(dst + i, element);
            *written += 1;
        });

Copilot · 2026-03-31T22:25:04Z

library/alloc/src/collections/vec_deque/mod.rs

 use core::ops::{Index, IndexMut, Range, RangeBounds};
 use core::{fmt, ptr, slice};

+use safety::{ensures, requires};


ensures is imported but never used in this module. This will trigger an unused-import warning in builds that lint warnings as errors; consider removing ensures from the import list or adding an #[allow(unused_imports)] on this use if intentional.

Suggested change

use safety::{ensures, requires};

use safety::requires;

Copilot · 2026-03-31T22:25:06Z

library/alloc/src/collections/vec_deque/mod.rs

    /// Moves an element out of the buffer
+    ///
+    /// # Safety
+    ///
+    /// May only be called if `off < self.capacity()`.
    #[inline]
+    #[requires(off < self.capacity())]
+    #[cfg_attr(kani, kani::modifies(self))]
    unsafe fn buffer_read(&mut self, off: usize) -> T {
        unsafe { ptr::read(self.ptr().add(off)) }


The safety contract for buffer_read is too weak for the operation it performs. ptr::read(self.ptr().add(off)) is UB if the slot at off is uninitialized (even if off < capacity()), so the precondition/docs should also require that off refers to an initialized element (e.g., corresponds to some logical index < self.len).

Copilot · 2026-03-31T22:25:07Z

library/alloc/src/collections/vec_deque/mod.rs

    /// Writes all values from `iter` to `dst`, wrapping
    /// at the end of the buffer and returns the number
    /// of written values.
    ///
    /// # Safety
    ///
    /// Assumes that `iter` yields at most `len` items.
    /// Assumes capacity is sufficient.
+    #[requires(dst < self.capacity() && len <= self.capacity())]
+    #[cfg_attr(kani, kani::modifies(
+        self,
+        core::ptr::slice_from_raw_parts_mut(self.ptr(), self.capacity())
+    ))]
    unsafe fn write_iter_wrapping(


write_iter_wrapping’s #[requires] is missing the key safety assumption documented in the comment: that iter yields at most len items. Without that, the calls to write_iter can still write past the end of the ring buffer. Consider expressing an iterator upper bound in the contract (or changing the function to accept an iterator with a known length).

Copilot · 2026-03-31T22:25:08Z

library/alloc/src/collections/vec_deque/mod.rs

    #[inline]
+    #[requires(old_capacity <= self.capacity() && self.len <= old_capacity)]


handle_capacity_increase uses old_capacity - self.head and other arithmetic assuming self.head < old_capacity (or old_capacity == 0). The current #[requires] doesn’t constrain self.head relative to old_capacity, so callers satisfying the stated preconditions can still trigger underflow and subsequent out-of-bounds copies. Consider strengthening the contract (and safety docs) to include old_capacity == 0 || self.head < old_capacity.

Suggested change

#[inline]

#[requires(old_capacity <= self.capacity() && self.len <= old_capacity)]

/// Additionally, `old_capacity == 0` or `self.head < old_capacity` must hold.

#[inline]

#[requires(

old_capacity <= self.capacity()

&& self.len <= old_capacity

&& (old_capacity == 0 || self.head < old_capacity)

)]

Copilot · 2026-03-31T22:25:10Z

doc/src/challenges/0025-vecdeque.md

+| `abort_shrink` | `target_cap <= cap && len <= target_cap && old_head < cap` | `check_abort_shrink` |
+| `rotate_left_inner` | `mid <= self.len() / 2` | `check_rotate_left_inner` |
+| `rotate_right_inner` | `k <= self.len() / 2` | `check_rotate_right_inner` |
+


The verification summary claims "All 13 Part A unsafe functions" were verified, but the table lists 15 functions (it includes rotate_left_inner and rotate_right_inner). Please reconcile the counts/text so the summary matches what’s actually covered.

Suggested change

Note: The core Part A includes 13 unsafe functions. The two internal helpers

`rotate_left_inner` and `rotate_right_inner` are listed here and verified as

well, but are not counted among those 13 Part A unsafe functions.

Copilot · 2026-03-31T22:25:10Z

library/alloc/src/collections/vec_deque/mod.rs

    /// Copies a contiguous block of memory len long from src to dst
+    ///
+    /// # Safety
+    ///
+    /// `src + len` and `dst + len` must not exceed `self.capacity()`.
    #[inline]
+    #[requires(len <= self.capacity() && src <= self.capacity() - len && dst <= self.capacity() - len)]
+    #[cfg_attr(kani, kani::modifies(
+        core::ptr::slice_from_raw_parts_mut(self.ptr().add(dst), len)
+    ))]
    unsafe fn copy(&mut self, src: usize, dst: usize, len: usize) {


The copy safety contract only constrains src/dst/len to be in-bounds, but ptr::copy(self.ptr().add(src), ...) also requires the source range to be initialized for T (reading uninitialized T is UB). If the intent is to fully formalize the unsafe preconditions, the contract/docs should also state that src..src+len refers to initialized elements in the buffer (and that the destination is valid for writes).

Samuelsills force-pushed the challenge-25-vecdeque branch from 40ae507 to 10224fd Compare March 24, 2026 16:45

Samuelsills force-pushed the challenge-25-vecdeque branch from 10224fd to 2a16efd Compare March 24, 2026 17:01

Samuelsills marked this pull request as ready for review March 24, 2026 20:50

Samuelsills requested a review from a team as a code owner March 24, 2026 20:50

feliperodri added the Challenge Used to tag a challenge label Mar 25, 2026

feliperodri requested a review from Copilot March 31, 2026 22:18

Copilot started reviewing on behalf of feliperodri March 31, 2026 22:18 View session

Copilot AI reviewed Mar 31, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Challenge 25: Verify safety of VecDeque#564

Challenge 25: Verify safety of VecDeque#564
Samuelsills wants to merge 1 commit intomodel-checking:mainfrom
Samuelsills:challenge-25-vecdeque

Samuelsills commented Mar 24, 2026

Uh oh!

Samuelsills commented Mar 29, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		#[inline]
		#[requires(old_capacity <= self.capacity() && self.len <= old_capacity)]

+Note: The core Part A includes 13 unsafe functions. The two internal helpers
+`rotate_left_inner` and `rotate_right_inner` are listed here and verified as
+well, but are not counted among those 13 Part A unsafe functions.

Conversation

Samuelsills commented Mar 24, 2026

Summary

Uh oh!

Samuelsills commented Mar 29, 2026

Verification Coverage Report

Unsafe Functions (13/13 — contracts written and verified)

Safe Abstractions (30/30 — absence of UB verified)

UBs Checked (automatic via Kani/CBMC)

Verification Approach

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants